﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;
using System.Numerics;

namespace OverSATb
{
    public class SatSolver
    {
        
        class Variable
        {
            public int Name;
            public int ColumnIndex;
            public BigInteger AssignMask;
        }

        class Clause
        {
            public List<int> VariableReferences = new List<int>();
            public uint NotBits;
            public uint NotBitMask;

            public Tuple CreateTuple( uint localBits )
            {
                Tuple t = new Tuple();
                uint bitIndex = 1;
                int count = 0;
                while (count < VariableReferences.Count)
                {
                    var c = VariableReferences[count];
                    t.Assignments.Add(new Assign
                    {
                        NameId = c,
                        Value = ((localBits & bitIndex) > 0) ? 1u : 0
                    });
                    bitIndex <<= 1;
                    count++;
                }
                return t;
            }

            /// <summary>
            /// Test returns true if the local bits given actually evaluate to true in a SAT clause
            /// </summary>
            /// <param name="localBits"></param>
            /// <returns></returns>
            public bool Test( uint localBits )
            {
                uint BitsThatAreNotted = localBits & NotBits;
                uint NottedValues = BitsThatAreNotted ^ NotBits;
                uint OtherValues = localBits & NotBitMask;
                return (NottedValues > 0 || OtherValues > 0);
            }

        }

        List<Clause> Clauses = new List<Clause>();
        List<Variable> Variables = new List<Variable>();
        Dictionary<int, Variable> VariablesById = new Dictionary<int, Variable>();
        private int CurrentColumnIndex = 0;

        public BigInteger TotalRows = 0;
        public List<Tuple> DeletedTuples = new List<Tuple>();

        public uint GetValue(int nameId, BigInteger rowIdx)
        {
            Variable v = VariablesById[nameId];
            uint vn = (v.AssignMask & rowIdx) > 0 ? 1u : 0u;
            return vn;
        }

        public Range GetNextMatchingRange(int nameId, BigInteger searchRowIdx, uint searchValue)
        {
            Range result = new Range();

            Variable v = VariablesById[nameId];

            uint value = (v.AssignMask & searchRowIdx) > 0 ? 1u : 0u; 
            BigInteger band = v.AssignMask * 2;

            if (value == searchValue)
            {
                result.Start = searchRowIdx;
                result.Stop = result.Start + (v.AssignMask - result.Start % v.AssignMask);
                result.Empty = false;
            }
            else if (value < searchValue)
            {
                BigInteger delta = (searchValue - value) * v.AssignMask;
                result.Start = (searchRowIdx / v.AssignMask) * v.AssignMask + delta;
                result.Stop = result.Start + (v.AssignMask - result.Start % v.AssignMask);
                result.Empty = false;
            }
            else
            {
                result.Start = (((searchRowIdx / band) + 1) * band) + (searchValue * v.AssignMask);
                result.Stop = result.Start + (v.AssignMask - result.Start % v.AssignMask);
                result.Empty = false;
            }

            return result;
        }

        public Range GetNextMatchingRange(Tuple tuple, BigInteger startSearchRow)
        {
            Range newRange = new Range();
            newRange.Start = new BigInteger(0);
            newRange.Stop = TotalRows;

            foreach (var a in tuple.Assignments)
            {
                Range temp = GetNextMatchingRange(a.NameId, startSearchRow, a.Value);
                newRange = newRange.Intersection(temp);
            }

            return newRange;
        }


        public void AddClause(IEnumerable<int> cnfStyleVariables)
        {
            Clause c = new Clause();

            uint clauseBitIndex = 1;

            foreach (var n in cnfStyleVariables)
            {
                int nameId;
                if (n < 0)
                {
                    c.NotBits |= clauseBitIndex;
                    nameId = -n;
                }
                else
                {
                    nameId = n;
                }
                c.VariableReferences.Add(nameId);
                clauseBitIndex <<= 1;
                if (!VariablesById.ContainsKey(nameId))
                {
                    BigInteger mask = new BigInteger(1);
                    mask <<= CurrentColumnIndex;
                    Variable v = new Variable {
                        ColumnIndex = CurrentColumnIndex,
                        Name = nameId,
                        AssignMask = mask
                    };
                    Variables.Add(v);
                    VariablesById.Add(nameId, v);
                    if (TotalRows == BigInteger.Zero)
                    {
                        TotalRows = 2;
                    }
                    else
                    {
                        TotalRows *= 2;
                    }
                    CurrentColumnIndex++;
                }
            }

            c.NotBitMask = ~c.NotBits;

            // now, generate deletes

            for (uint bt = 0; bt < clauseBitIndex; bt++)
            {
                var t = c.Test(bt);
                if (!t)
                {
                    var delTupe = c.CreateTuple(bt);
                    DeletedTuples.Add(delTupe);
                }
            }

            Clauses.Add(c);
        }

        public Tuple GetValueAtRow(BigInteger rowIdx)
        {
            Tuple t = new Tuple();

            foreach (var col in Variables)
            {
                var assign = new Assign();
                assign.NameId = col.Name;
                assign.Value = GetValue(assign.NameId, rowIdx);
                t.Assignments.Add(assign);
            }

            return t;
        }

        BigInteger GetNextTrueRow(BigInteger firstSearchRowIdx)
        {
            bool found = false;
            BigInteger row = firstSearchRowIdx;

            while (!found)
            {
                BigInteger deletedMin = row;
                found = true;
                foreach (var tuple in DeletedTuples)
                {
                    Range t = GetNextMatchingRange(tuple, row);
                    if (t.Contains(row))
                    {
                        deletedMin = t.Stop >= deletedMin ? t.Stop : deletedMin;
                        row = deletedMin;
                        found = false;
                        break;
                    }
                }
            }

            return row;
        }

        public static void Test()
        {
            SatSolver solver = new SatSolver();

            solver.AddClause( new int[] { -1, 2, 3 } );
            solver.AddClause( new int[] { 1, -4, 5 } );
            solver.AddClause( new int[] { 4, 5, 7 } );

            BigInteger row = 0;

            do
            {
                var nextRow = solver.GetNextTrueRow(row);
                if (nextRow < solver.TotalRows)
                {
                    var result = solver.GetValueAtRow(nextRow);
                }
                row = nextRow;
            }
            while (row < solver.TotalRows);
        }

    }
}
